(0) Obligation:

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), 0).
quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U).
quot(X, Y, Z, U) :- ','(no(zero(X)), ','(no(zero(Y)), ','(p(X, Px), ','(p(Y, Py), quot(Px, Py, Z, U))))).
p(0, 0).
p(s(X), X).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X1).
failure(b).

Query: div(g,g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(2) Obligation:

Clauses:

quotA(0, 0).
quotA(s(T106), s(T108)) :- quotA(T106, T108).
quotB(0, 0).
quotB(s(0), 0).
quotB(s(s(T230)), s(T232)) :- quotB(T230, T232).
quotC(0, 0).
quotC(s(0), 0).
quotC(s(s(0)), 0).
quotC(s(s(s(T372))), s(T374)) :- quotC(T372, T374).
quotD(0, 0).
quotD(s(0), 0).
quotD(s(s(0)), 0).
quotD(s(s(s(0))), 0).
quotD(s(s(s(s(T532)))), s(T534)) :- quotD(T532, T534).
quotE(0, 0).
quotE(s(0), 0).
quotE(s(s(0)), 0).
quotE(s(s(s(0))), 0).
quotE(s(s(s(s(0)))), 0).
quotE(s(s(s(s(s(T710))))), s(T712)) :- quotE(T710, T712).
quotF(0, 0).
quotF(s(0), 0).
quotF(s(s(0)), 0).
quotF(s(s(s(0))), 0).
quotF(s(s(s(s(0)))), 0).
quotF(s(s(s(s(s(0))))), 0).
quotF(s(s(s(s(s(s(T906)))))), s(T908)) :- quotF(T906, T908).
quotG(0, 0).
quotG(s(0), 0).
quotG(s(s(0)), 0).
quotG(s(s(s(0))), 0).
quotG(s(s(s(s(0)))), 0).
quotG(s(s(s(s(s(0))))), 0).
quotG(s(s(s(s(s(s(0)))))), 0).
quotG(s(s(s(s(s(s(s(T1120))))))), s(T1122)) :- quotG(T1120, T1122).
quotH(0, s(T15), 0).
quotH(s(0), s(s(T68)), 0).
quotH(s(T77), s(0), s(T79)) :- quotA(T77, T79).
quotH(s(s(0)), s(s(s(T174))), 0).
quotH(s(s(T183)), s(s(0)), s(T185)) :- quotB(T183, T185).
quotH(s(s(s(0))), s(s(s(s(T298)))), 0).
quotH(s(s(s(T307))), s(s(s(0))), s(T309)) :- quotC(T307, T309).
quotH(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0).
quotH(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) :- quotD(T449, T451).
quotH(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0).
quotH(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) :- quotE(T609, T611).
quotH(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0).
quotH(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) :- quotF(T787, T789).
quotH(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0).
quotH(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) :- quotG(T983, T985).
quotH(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) :- quotI(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149).
quotI(0, s(T1197), T1198, 0).
quotI(T1211, 0, T1212, s(T1214)) :- quotH(T1211, s(T1212), T1214).
quotI(s(T1261), s(T1266), T1230, T1232) :- quotI(T1261, T1266, T1230, T1232).
divJ(T7, T8, T10) :- quotH(T7, T8, T10).

Query: divJ(g,g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
divJ_in: (b,b,f)
quotH_in: (b,b,f)
quotA_in: (b,f)
quotB_in: (b,f)
quotC_in: (b,f)
quotD_in: (b,f)
quotE_in: (b,f)
quotF_in: (b,f)
quotG_in: (b,f)
quotI_in: (b,b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

DIVJ_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quotH_in_gga(T7, T8, T10))
DIVJ_IN_GGA(T7, T8, T10) → QUOTH_IN_GGA(T7, T8, T10)
QUOTH_IN_GGA(s(T77), s(0), s(T79)) → U8_GGA(T77, T79, quotA_in_ga(T77, T79))
QUOTH_IN_GGA(s(T77), s(0), s(T79)) → QUOTA_IN_GA(T77, T79)
QUOTA_IN_GA(s(T106), s(T108)) → U1_GA(T106, T108, quotA_in_ga(T106, T108))
QUOTA_IN_GA(s(T106), s(T108)) → QUOTA_IN_GA(T106, T108)
QUOTH_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → U9_GGA(T183, T185, quotB_in_ga(T183, T185))
QUOTH_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → QUOTB_IN_GA(T183, T185)
QUOTB_IN_GA(s(s(T230)), s(T232)) → U2_GA(T230, T232, quotB_in_ga(T230, T232))
QUOTB_IN_GA(s(s(T230)), s(T232)) → QUOTB_IN_GA(T230, T232)
QUOTH_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_GGA(T307, T309, quotC_in_ga(T307, T309))
QUOTH_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → QUOTC_IN_GA(T307, T309)
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → U3_GA(T372, T374, quotC_in_ga(T372, T374))
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → QUOTC_IN_GA(T372, T374)
QUOTH_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_GGA(T449, T451, quotD_in_ga(T449, T451))
QUOTH_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → QUOTD_IN_GA(T449, T451)
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → U4_GA(T532, T534, quotD_in_ga(T532, T534))
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTD_IN_GA(T532, T534)
QUOTH_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_GGA(T609, T611, quotE_in_ga(T609, T611))
QUOTH_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → QUOTE_IN_GA(T609, T611)
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → U5_GA(T710, T712, quotE_in_ga(T710, T712))
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTE_IN_GA(T710, T712)
QUOTH_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_GGA(T787, T789, quotF_in_ga(T787, T789))
QUOTH_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → QUOTF_IN_GA(T787, T789)
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → U6_GA(T906, T908, quotF_in_ga(T906, T908))
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTF_IN_GA(T906, T908)
QUOTH_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_GGA(T983, T985, quotG_in_ga(T983, T985))
QUOTH_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → QUOTG_IN_GA(T983, T985)
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_GA(T1120, T1122, quotG_in_ga(T1120, T1122))
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTG_IN_GA(T1120, T1122)
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_GGA(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → U16_GGGA(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTH_IN_GGA(T1211, s(T1212), T1214)
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → U17_GGGA(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTI_IN_GGGA(T1261, T1266, T1230, T1232)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
DIVJ_IN_GGA(x1, x2, x3)  =  DIVJ_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
QUOTH_IN_GGA(x1, x2, x3)  =  QUOTH_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
QUOTA_IN_GA(x1, x2)  =  QUOTA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
QUOTB_IN_GA(x1, x2)  =  QUOTB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x4)
QUOTI_IN_GGGA(x1, x2, x3, x4)  =  QUOTI_IN_GGGA(x1, x2, x3)
U16_GGGA(x1, x2, x3, x4)  =  U16_GGGA(x4)
U17_GGGA(x1, x2, x3, x4, x5)  =  U17_GGGA(x5)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DIVJ_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quotH_in_gga(T7, T8, T10))
DIVJ_IN_GGA(T7, T8, T10) → QUOTH_IN_GGA(T7, T8, T10)
QUOTH_IN_GGA(s(T77), s(0), s(T79)) → U8_GGA(T77, T79, quotA_in_ga(T77, T79))
QUOTH_IN_GGA(s(T77), s(0), s(T79)) → QUOTA_IN_GA(T77, T79)
QUOTA_IN_GA(s(T106), s(T108)) → U1_GA(T106, T108, quotA_in_ga(T106, T108))
QUOTA_IN_GA(s(T106), s(T108)) → QUOTA_IN_GA(T106, T108)
QUOTH_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → U9_GGA(T183, T185, quotB_in_ga(T183, T185))
QUOTH_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → QUOTB_IN_GA(T183, T185)
QUOTB_IN_GA(s(s(T230)), s(T232)) → U2_GA(T230, T232, quotB_in_ga(T230, T232))
QUOTB_IN_GA(s(s(T230)), s(T232)) → QUOTB_IN_GA(T230, T232)
QUOTH_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_GGA(T307, T309, quotC_in_ga(T307, T309))
QUOTH_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → QUOTC_IN_GA(T307, T309)
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → U3_GA(T372, T374, quotC_in_ga(T372, T374))
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → QUOTC_IN_GA(T372, T374)
QUOTH_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_GGA(T449, T451, quotD_in_ga(T449, T451))
QUOTH_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → QUOTD_IN_GA(T449, T451)
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → U4_GA(T532, T534, quotD_in_ga(T532, T534))
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTD_IN_GA(T532, T534)
QUOTH_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_GGA(T609, T611, quotE_in_ga(T609, T611))
QUOTH_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → QUOTE_IN_GA(T609, T611)
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → U5_GA(T710, T712, quotE_in_ga(T710, T712))
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTE_IN_GA(T710, T712)
QUOTH_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_GGA(T787, T789, quotF_in_ga(T787, T789))
QUOTH_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → QUOTF_IN_GA(T787, T789)
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → U6_GA(T906, T908, quotF_in_ga(T906, T908))
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTF_IN_GA(T906, T908)
QUOTH_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_GGA(T983, T985, quotG_in_ga(T983, T985))
QUOTH_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → QUOTG_IN_GA(T983, T985)
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_GA(T1120, T1122, quotG_in_ga(T1120, T1122))
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTG_IN_GA(T1120, T1122)
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_GGA(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → U16_GGGA(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTH_IN_GGA(T1211, s(T1212), T1214)
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → U17_GGGA(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTI_IN_GGGA(T1261, T1266, T1230, T1232)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
DIVJ_IN_GGA(x1, x2, x3)  =  DIVJ_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
QUOTH_IN_GGA(x1, x2, x3)  =  QUOTH_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
QUOTA_IN_GA(x1, x2)  =  QUOTA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
QUOTB_IN_GA(x1, x2)  =  QUOTB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x4)
QUOTI_IN_GGGA(x1, x2, x3, x4)  =  QUOTI_IN_GGGA(x1, x2, x3)
U16_GGGA(x1, x2, x3, x4)  =  U16_GGGA(x4)
U17_GGGA(x1, x2, x3, x4, x5)  =  U17_GGGA(x5)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 8 SCCs with 26 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTG_IN_GA(T1120, T1122)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTG_IN_GA(T1120, T1122)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTG_IN_GA(s(s(s(s(s(s(s(T1120)))))))) → QUOTG_IN_GA(T1120)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTG_IN_GA(s(s(s(s(s(s(s(T1120)))))))) → QUOTG_IN_GA(T1120)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTF_IN_GA(T906, T908)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTF_IN_GA(T906, T908)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTF_IN_GA(s(s(s(s(s(s(T906))))))) → QUOTF_IN_GA(T906)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTF_IN_GA(s(s(s(s(s(s(T906))))))) → QUOTF_IN_GA(T906)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTE_IN_GA(T710, T712)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTE_IN_GA(T710, T712)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTE_IN_GA(s(s(s(s(s(T710)))))) → QUOTE_IN_GA(T710)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTE_IN_GA(s(s(s(s(s(T710)))))) → QUOTE_IN_GA(T710)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTD_IN_GA(T532, T534)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTD_IN_GA(T532, T534)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTD_IN_GA(s(s(s(s(T532))))) → QUOTD_IN_GA(T532)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTD_IN_GA(s(s(s(s(T532))))) → QUOTD_IN_GA(T532)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTC_IN_GA(s(s(s(T372))), s(T374)) → QUOTC_IN_GA(T372, T374)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTC_IN_GA(s(s(s(T372))), s(T374)) → QUOTC_IN_GA(T372, T374)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTC_IN_GA(s(s(s(T372)))) → QUOTC_IN_GA(T372)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTC_IN_GA(s(s(s(T372)))) → QUOTC_IN_GA(T372)
    The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTB_IN_GA(s(s(T230)), s(T232)) → QUOTB_IN_GA(T230, T232)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTB_IN_GA(x1, x2)  =  QUOTB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTB_IN_GA(s(s(T230)), s(T232)) → QUOTB_IN_GA(T230, T232)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTB_IN_GA(x1, x2)  =  QUOTB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTB_IN_GA(s(s(T230))) → QUOTB_IN_GA(T230)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTB_IN_GA(s(s(T230))) → QUOTB_IN_GA(T230)
    The graph contains the following edges 1 > 1

(50) YES

(51) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTA_IN_GA(s(T106), s(T108)) → QUOTA_IN_GA(T106, T108)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTA_IN_GA(x1, x2)  =  QUOTA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(52) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(53) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTA_IN_GA(s(T106), s(T108)) → QUOTA_IN_GA(T106, T108)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOTA_IN_GA(x1, x2)  =  QUOTA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(54) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTA_IN_GA(s(T106)) → QUOTA_IN_GA(T106)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(56) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTA_IN_GA(s(T106)) → QUOTA_IN_GA(T106)
    The graph contains the following edges 1 > 1

(57) YES

(58) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTH_IN_GGA(T1211, s(T1212), T1214)
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTI_IN_GGGA(T1261, T1266, T1230, T1232)

The TRS R consists of the following rules:

divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divJ_in_gga(x1, x2, x3)  =  divJ_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quotH_in_gga(x1, x2, x3)  =  quotH_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotH_out_gga(x1, x2, x3)  =  quotH_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quotA_in_ga(x1, x2)  =  quotA_in_ga(x1)
quotA_out_ga(x1, x2)  =  quotA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quotB_in_ga(x1, x2)  =  quotB_in_ga(x1)
quotB_out_ga(x1, x2)  =  quotB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
quotI_in_ggga(x1, x2, x3, x4)  =  quotI_in_ggga(x1, x2, x3)
quotI_out_ggga(x1, x2, x3, x4)  =  quotI_out_ggga(x4)
U16_ggga(x1, x2, x3, x4)  =  U16_ggga(x4)
U17_ggga(x1, x2, x3, x4, x5)  =  U17_ggga(x5)
divJ_out_gga(x1, x2, x3)  =  divJ_out_gga(x3)
QUOTH_IN_GGA(x1, x2, x3)  =  QUOTH_IN_GGA(x1, x2)
QUOTI_IN_GGGA(x1, x2, x3, x4)  =  QUOTI_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(59) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(60) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTH_IN_GGA(T1211, s(T1212), T1214)
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTI_IN_GGGA(T1261, T1266, T1230, T1232)

R is empty.
The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
QUOTH_IN_GGA(x1, x2, x3)  =  QUOTH_IN_GGA(x1, x2)
QUOTI_IN_GGGA(x1, x2, x3, x4)  =  QUOTI_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(61) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181))))))))) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))))
QUOTI_IN_GGGA(T1211, 0, T1212) → QUOTH_IN_GGA(T1211, s(T1212))
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230) → QUOTI_IN_GGGA(T1261, T1266, T1230)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(63) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOTI_IN_GGGA(T1211, 0, T1212) → QUOTH_IN_GGA(T1211, s(T1212))
    The graph contains the following edges 1 >= 1

  • QUOTI_IN_GGGA(s(T1261), s(T1266), T1230) → QUOTI_IN_GGGA(T1261, T1266, T1230)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181))))))))) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

(64) YES